COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	book[f85,jmc]		Some notes for revising McCarthy and Talcott
C00005 ENDMK
C⊗;
book[f85,jmc]		Some notes for revising McCarthy and Talcott

1985 Dec 13

1. The students seem to have learned the proving in CS306 in Fall 1985
better than at any previous time judging from the take-home final.
The problem, associativity and commutativity of set union
with sets represented as lists without repetitions together
with the distributivity of union and intersection produced long
writeups with many lemmas.  It is a good problem to put in the
book itself and to do in EKL.  Moreover, it provides a good
example for the problem of improving interactive theorem provers.
It would be interesting to see how well Boyer-Moore does; it might
invent some of the needed lemmas.

Remark: If it were proved that the operations actually implement
the set operations, then the desired properties would follow from
that fact and set theory.  This isn't the way anyone did it, but
it is probably the best way to go in the long run.

As for CS306, it is necessary to be more efficient in the future
with the lectures.  EKL should be introduced even sooner.  I need
a heavy duty LISPAX, and good initial example, e.g. set operations,
and another example for them to do.

2. Book needs section on derived functions, presumably with the
cons counter maker as an explicit example.

3. Call-by-need as an example macro.  There needs to be a corresponding
macro exercise and a corresponding exercise and example exam question.